| Up | groups 1 |
| Definitions of Statement | IsMonoid(T;op;id), GrpSig, Mon, AbMon, IsMonHom{M1,M2}(f), IsMonHomInj(g;h;f), MonHom(M1,M2), OCMon |
| Definitions |   x,y. t(x;y),  , t  T, x f y, P & Q,  x:A. B(x), P   Q,  x:A. B(x), Mon, AbMon, OCMon, IsMonoid(T;op;id), IsMonHom{M1,M2}(f), MonHom(M1,M2), Order(T;x,y.R(x;y)), Linorder(T;x,y.R(x;y)), fun_thru_1op(A;B;opa;opb;f), x(s1,s2), IsMonHomInj(g;h;f), FunThru2op(A;B;opa;opb;f) |
| Lemmas | grp sig wf, grp le wf, grp eq wf, assert wf, rels iso wf, mon hom inj p wf, grp car wf, ocmon wf, eqfun p wf, grp id wf, monoid p wf, mon properties, comm wf, mon wf, abmonoid properties, monot wf, grp op wf, cancel wf, linorder wf, abmonoid wf, ocmon properties, assoc shift, monoid hom p wf, ident mon hom shift, eqfun p shift, comm shift, refl shift, trans shift, anti sym shift, connex shift, cancel shift, monot shift |
|h|
(x =
y);x,y.